The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

f(C(x1, x2)) → C(f(x1), f(x2))
f(Z) → Z
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2))
eqZList(C(x1, x2), Z) → False
eqZList(Z, C(y1, y2)) → False
eqZList(Z, Z) → True
second(C(x1, x2)) → x2
first(C(x1, x2)) → x1
g(x) → x

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True

Rewrite Strategy: INNERMOST

(1) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed relative TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

f(C(x1, x2)) → C(f(x1), f(x2)) [1]
f(Z) → Z [1]
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2)) [1]
eqZList(C(x1, x2), Z) → False [1]
eqZList(Z, C(y1, y2)) → False [1]
eqZList(Z, Z) → True [1]
second(C(x1, x2)) → x2 [1]
first(C(x1, x2)) → x1 [1]
g(x) → x [1]
and(False, False) → False [0]
and(True, False) → False [0]
and(False, True) → False [0]
and(True, True) → True [0]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

f(C(x1, x2)) → C(f(x1), f(x2)) [1]
f(Z) → Z [1]
eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2)) [1]
eqZList(C(x1, x2), Z) → False [1]
eqZList(Z, C(y1, y2)) → False [1]
eqZList(Z, Z) → True [1]
second(C(x1, x2)) → x2 [1]
first(C(x1, x2)) → x1 [1]
g(x) → x [1]
and(False, False) → False [0]
and(True, False) → False [0]
and(False, True) → False [0]
and(True, True) → True [0]

The TRS has the following type information:

f :: C:Z → C:Z C :: C:Z → C:Z → C:Z Z :: C:Z eqZList :: C:Z → C:Z → False:True and :: False:True → False:True → False:True False :: False:True True :: False:True second :: C:Z → C:Z first :: C:Z → C:Z g :: g → g

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

and(v0, v1) → null_and [0]
second(v0) → null_second [0]
first(v0) → null_first [0]
f(v0) → null_f [0]
eqZList(v0, v1) → null_eqZList [0]

And the following fresh constants:

null_and, null_second, null_first, null_f, null_eqZList, const

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: f(C(x1, x2)) → C(f(x1), f(x2)) [1] f(Z) → Z [1] eqZList(C(x1, x2), C(y1, y2)) → and(eqZList(x1, y1), eqZList(x2, y2)) [1] eqZList(C(x1, x2), Z) → False [1] eqZList(Z, C(y1, y2)) → False [1] eqZList(Z, Z) → True [1] second(C(x1, x2)) → x2 [1] first(C(x1, x2)) → x1 [1] g(x) → x [1] and(False, False) → False [0] and(True, False) → False [0] and(False, True) → False [0] and(True, True) → True [0] and(v0, v1) → null_and [0] second(v0) → null_second [0] first(v0) → null_first [0] f(v0) → null_f [0] eqZList(v0, v1) → null_eqZList [0] The TRS has the following type information: f :: C:Z:null_second:null_first:null_f → C:Z:null_second:null_first:null_f C :: C:Z:null_second:null_first:null_f → C:Z:null_second:null_first:null_f → C:Z:null_second:null_first:null_f Z :: C:Z:null_second:null_first:null_f eqZList :: C:Z:null_second:null_first:null_f → C:Z:null_second:null_first:null_f → False:True:null_and:null_eqZList and :: False:True:null_and:null_eqZList → False:True:null_and:null_eqZList → False:True:null_and:null_eqZList False :: False:True:null_and:null_eqZList True :: False:True:null_and:null_eqZList second :: C:Z:null_second:null_first:null_f → C:Z:null_second:null_first:null_f first :: C:Z:null_second:null_first:null_f → C:Z:null_second:null_first:null_f g :: g → g null_and :: False:True:null_and:null_eqZList null_second :: C:Z:null_second:null_first:null_f null_first :: C:Z:null_second:null_first:null_f null_f :: C:Z:null_second:null_first:null_f null_eqZList :: False:True:null_and:null_eqZList const :: g Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

Z => 0
False => 1
True => 2
null_and => 0
null_second => 0
null_first => 0
null_f => 0
null_eqZList => 0
const => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

and(z, z') -{ 0 }→ 2 :|: z = 2, z' = 2
and(z, z') -{ 0 }→ 1 :|: z = 1, z' = 1
and(z, z') -{ 0 }→ 1 :|: z = 2, z' = 1
and(z, z') -{ 0 }→ 1 :|: z' = 2, z = 1
and(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
eqZList(z, z') -{ 1 }→ and(eqZList(x1, y1), eqZList(x2, y2)) :|: y1 >= 0, x1 >= 0, z' = 1 + y1 + y2, z = 1 + x1 + x2, y2 >= 0, x2 >= 0
eqZList(z, z') -{ 1 }→ 2 :|: z = 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = 0
eqZList(z, z') -{ 1 }→ 1 :|: y1 >= 0, z' = 1 + y1 + y2, y2 >= 0, z = 0
eqZList(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
f(z) -{ 1 }→ 0 :|: z = 0
f(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
f(z) -{ 1 }→ 1 + f(x1) + f(x2) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
g(z) -{ 1 }→ x :|: x >= 0, z = x
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V3),0,[f(V, Out)],[V >= 0]). eq(start(V, V3),0,[eqZList(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3),0,[second(V, Out)],[V >= 0]). eq(start(V, V3),0,[first(V, Out)],[V >= 0]). eq(start(V, V3),0,[g(V, Out)],[V >= 0]). eq(start(V, V3),0,[and(V, V3, Out)],[V >= 0,V3 >= 0]). eq(f(V, Out),1,[f(V1, Ret01),f(V2, Ret1)],[Out = 1 + Ret01 + Ret1,V1 >= 0,V = 1 + V1 + V2,V2 >= 0]). eq(f(V, Out),1,[],[Out = 0,V = 0]). eq(eqZList(V, V3, Out),1,[eqZList(V4, V5, Ret0),eqZList(V6, V7, Ret11),and(Ret0, Ret11, Ret)],[Out = Ret,V5 >= 0,V4 >= 0,V3 = 1 + V5 + V7,V = 1 + V4 + V6,V7 >= 0,V6 >= 0]). eq(eqZList(V, V3, Out),1,[],[Out = 1,V8 >= 0,V = 1 + V8 + V9,V9 >= 0,V3 = 0]). eq(eqZList(V, V3, Out),1,[],[Out = 1,V10 >= 0,V3 = 1 + V10 + V11,V11 >= 0,V = 0]). eq(eqZList(V, V3, Out),1,[],[Out = 2,V = 0,V3 = 0]). eq(second(V, Out),1,[],[Out = V12,V13 >= 0,V = 1 + V12 + V13,V12 >= 0]). eq(first(V, Out),1,[],[Out = V14,V14 >= 0,V = 1 + V14 + V15,V15 >= 0]). eq(g(V, Out),1,[],[Out = V16,V16 >= 0,V = V16]). eq(and(V, V3, Out),0,[],[Out = 1,V = 1,V3 = 1]). eq(and(V, V3, Out),0,[],[Out = 1,V = 2,V3 = 1]). eq(and(V, V3, Out),0,[],[Out = 1,V3 = 2,V = 1]). eq(and(V, V3, Out),0,[],[Out = 2,V = 2,V3 = 2]). eq(and(V, V3, Out),0,[],[Out = 0,V17 >= 0,V18 >= 0,V = V17,V3 = V18]). eq(second(V, Out),0,[],[Out = 0,V19 >= 0,V = V19]). eq(first(V, Out),0,[],[Out = 0,V20 >= 0,V = V20]). eq(f(V, Out),0,[],[Out = 0,V21 >= 0,V = V21]). eq(eqZList(V, V3, Out),0,[],[Out = 0,V22 >= 0,V23 >= 0,V = V22,V3 = V23]). input_output_vars(f(V,Out),[V],[Out]). input_output_vars(eqZList(V,V3,Out),[V,V3],[Out]). input_output_vars(second(V,Out),[V],[Out]). input_output_vars(first(V,Out),[V],[Out]). input_output_vars(g(V,Out),[V],[Out]). input_output_vars(and(V,V3,Out),[V,V3],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. non_recursive : [and/3]
1. recursive [non_tail,multiple] : [eqZList/3]
2. recursive [multiple] : [f/2]
3. non_recursive : [first/2]
4. non_recursive : [g/2]
5. non_recursive : [second/2]
6. non_recursive : [start/2]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into and/3
1. SCC is partially evaluated into eqZList/3
2. SCC is partially evaluated into f/2
3. SCC is partially evaluated into first/2
4. SCC is completely evaluated into other SCCs
5. SCC is partially evaluated into second/2
6. SCC is partially evaluated into start/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations and/3
* CE 24 is refined into CE [25]
* CE 23 is refined into CE [26]
* CE 21 is refined into CE [27]
* CE 22 is refined into CE [28]
* CE 20 is refined into CE [29]


### Cost equations --> "Loop" of and/3
* CEs [25] --> Loop 18
* CEs [26] --> Loop 19
* CEs [27] --> Loop 20
* CEs [28] --> Loop 21
* CEs [29] --> Loop 22

### Ranking functions of CR and(V,V3,Out)

#### Partial ranking functions of CR and(V,V3,Out)


### Specialization of cost equations eqZList/3
* CE 15 is refined into CE [30]
* CE 12 is refined into CE [31]
* CE 13 is refined into CE [32]
* CE 14 is refined into CE [33]
* CE 11 is refined into CE [34,35,36,37,38]


### Cost equations --> "Loop" of eqZList/3
* CEs [37] --> Loop 23
* CEs [36] --> Loop 24
* CEs [35] --> Loop 25
* CEs [34] --> Loop 26
* CEs [38] --> Loop 27
* CEs [30] --> Loop 28
* CEs [31] --> Loop 29
* CEs [32] --> Loop 30
* CEs [33] --> Loop 31

### Ranking functions of CR eqZList(V,V3,Out)
* RF of phase [23]: [V,V3]
* RF of phase [24,25,26]: [V,V3]
* RF of phase [27]: [V,V3]

#### Partial ranking functions of CR eqZList(V,V3,Out)
* Partial RF of phase [23]:
- RF of loop [23:1,23:2]:
V
V3
* Partial RF of phase [24,25,26]:
- RF of loop [24:1,24:2,25:1,25:2,26:1,26:2]:
V
V3
* Partial RF of phase [27]:
- RF of loop [27:1,27:2]:
V
V3


### Specialization of cost equations f/2
* CE 9 is refined into CE [39]
* CE 10 is refined into CE [40]
* CE 8 is refined into CE [41]


### Cost equations --> "Loop" of f/2
* CEs [41] --> Loop 32
* CEs [39,40] --> Loop 33

### Ranking functions of CR f(V,Out)
* RF of phase [32]: [V]

#### Partial ranking functions of CR f(V,Out)
* Partial RF of phase [32]:
- RF of loop [32:1,32:2]:
V


### Specialization of cost equations first/2
* CE 18 is refined into CE [42]
* CE 19 is refined into CE [43]


### Cost equations --> "Loop" of first/2
* CEs [42] --> Loop 34
* CEs [43] --> Loop 35

### Ranking functions of CR first(V,Out)

#### Partial ranking functions of CR first(V,Out)


### Specialization of cost equations second/2
* CE 16 is refined into CE [44]
* CE 17 is refined into CE [45]


### Cost equations --> "Loop" of second/2
* CEs [44] --> Loop 36
* CEs [45] --> Loop 37

### Ranking functions of CR second(V,Out)

#### Partial ranking functions of CR second(V,Out)


### Specialization of cost equations start/2
* CE 2 is refined into CE [46,47]
* CE 3 is refined into CE [48,49,50,51,52,53]
* CE 4 is refined into CE [54,55]
* CE 5 is refined into CE [56,57]
* CE 6 is refined into CE [58]
* CE 7 is refined into CE [59,60,61,62,63]


### Cost equations --> "Loop" of start/2
* CEs [50] --> Loop 38
* CEs [62] --> Loop 39
* CEs [61] --> Loop 40
* CEs [60] --> Loop 41
* CEs [53,59] --> Loop 42
* CEs [49] --> Loop 43
* CEs [46,47,48,51,52,54,55,56,57,58,63] --> Loop 44

### Ranking functions of CR start(V,V3)

#### Partial ranking functions of CR start(V,V3)


Computing Bounds
=====================================

#### Cost of chains of and(V,V3,Out):
* Chain [22]: 0
with precondition: [V=1,V3=1,Out=1]

* Chain [21]: 0
with precondition: [V=1,V3=2,Out=1]

* Chain [20]: 0
with precondition: [V=2,V3=1,Out=1]

* Chain [19]: 0
with precondition: [V=2,V3=2,Out=2]

* Chain [18]: 0
with precondition: [Out=0,V>=0,V3>=0]


#### Cost of chains of eqZList(V,V3,Out):
* Chain [31]: 1
with precondition: [V=0,V3=0,Out=2]

* Chain [30]: 1
with precondition: [V=0,Out=1,V3>=1]

* Chain [29]: 1
with precondition: [V3=0,Out=1,V>=1]

* Chain [28]: 0
with precondition: [Out=0,V>=0,V3>=0]

* Chain [multiple([27],[[multiple([24,25,26],[[multiple([23],[[31]])],[31],[30],[29]])],[multiple([23],[[31]])],[31],[30],[29],[28]])]: 1*it(27)+1*it([29])+1*it([30])+1*it([31])+5*s(1)+1*s(3)+1*s(4)+1*s(5)+1*s(6)+1*s(7)+0
Such that:aux(11) =< V
aux(12) =< V+1
aux(13) =< V/2+1/2
aux(14) =< V/3+V3/3+2/3
aux(15) =< V3+1
aux(16) =< V3/2+1/2
it(27) =< aux(11)
it([29]) =< aux(11)
it([29]) =< aux(12)
it([30]) =< aux(12)
it([31]) =< aux(12)
it([29]) =< aux(13)
it([31]) =< aux(15)
s(1) =< aux(15)
it([30]) =< aux(16)
s(11) =< aux(15)* (1/2)
s(9) =< aux(14)* (6/5)
s(6) =< aux(13)
s(5) =< aux(14)
s(3) =< s(9)
s(4) =< s(9)
s(5) =< s(9)
s(4) =< aux(15)
s(5) =< aux(15)
s(7) =< aux(15)
s(7) =< s(11)
s(5) =< s(1)* (1/3)+aux(14)
s(3) =< s(1)* (1/5)+s(9)
s(4) =< s(1)* (1/5)+s(9)
s(5) =< s(1)* (1/5)+s(9)

with precondition: [Out=0,V>=1,V3>=1]

* Chain [multiple([24,25,26],[[multiple([23],[[31]])],[31],[30],[29]])]: 1*it(24)+1*it(25)+1*it(26)+1*it([29])+1*it([30])+3*it([31])+0
Such that:aux(3) =< V/2+1/2
aux(4) =< V/3+V3/3
aux(5) =< 2/5*V+2/5*V3
aux(6) =< V3
aux(7) =< V3+1
aux(8) =< V3/2+1/2
it([29]) =< aux(3)
it(26) =< aux(4)
it(24) =< aux(5)
it(25) =< aux(5)
it(26) =< aux(5)
it(25) =< aux(6)
it(26) =< aux(6)
it([30]) =< aux(6)
it([31]) =< aux(7)
it([30]) =< aux(8)
it(26) =< it([31])* (1/3)+aux(4)
it(24) =< it([31])* (1/5)+aux(5)
it(25) =< it([31])* (1/5)+aux(5)
it(26) =< it([31])* (1/5)+aux(5)

with precondition: [Out=1,V>=1,V3>=1,V+V3>=3]

* Chain [multiple([23],[[31]])]: 1*it(23)+1*it([31])+0
Such that:it(23) =< V3
it([31]) =< V3+1

with precondition: [Out=2,V=V3,V>=1]


#### Cost of chains of f(V,Out):
* Chain [33]: 1
with precondition: [Out=0,V>=0]

* Chain [multiple([32],[[33]])]: 1*it(32)+1*it([33])+0
Such that:it(32) =< V
it([33]) =< V+1

with precondition: [Out>=1,V>=Out]


#### Cost of chains of first(V,Out):
* Chain [35]: 0
with precondition: [Out=0,V>=0]

* Chain [34]: 1
with precondition: [Out>=0,V>=Out+1]


#### Cost of chains of second(V,Out):
* Chain [37]: 0
with precondition: [Out=0,V>=0]

* Chain [36]: 1
with precondition: [Out>=0,V>=Out+1]


#### Cost of chains of start(V,V3):
* Chain [44]: 2*s(33)+1*s(34)+1*s(42)+1*s(43)+1*s(44)+8*s(45)+2*s(48)+1*s(49)+1*s(50)+1*s(51)+1*s(52)+1*s(60)+1*s(61)+1*s(62)+1*s(63)+1
Such that:s(54) =< V/3+V3/3
s(38) =< V/3+V3/3+2/3
s(55) =< 2/5*V+2/5*V3
s(56) =< V3
aux(17) =< V
aux(18) =< V+1
aux(19) =< V/2+1/2
aux(20) =< V3+1
aux(21) =< V3/2+1/2
s(33) =< aux(17)
s(34) =< aux(18)
s(42) =< aux(17)
s(42) =< aux(18)
s(43) =< aux(18)
s(44) =< aux(18)
s(42) =< aux(19)
s(44) =< aux(20)
s(45) =< aux(20)
s(43) =< aux(21)
s(46) =< aux(20)* (1/2)
s(47) =< s(38)* (6/5)
s(48) =< aux(19)
s(49) =< s(38)
s(50) =< s(47)
s(51) =< s(47)
s(49) =< s(47)
s(51) =< aux(20)
s(49) =< aux(20)
s(52) =< aux(20)
s(52) =< s(46)
s(49) =< s(45)* (1/3)+s(38)
s(50) =< s(45)* (1/5)+s(47)
s(51) =< s(45)* (1/5)+s(47)
s(49) =< s(45)* (1/5)+s(47)
s(60) =< s(54)
s(61) =< s(55)
s(62) =< s(55)
s(60) =< s(55)
s(62) =< s(56)
s(60) =< s(56)
s(63) =< s(56)
s(63) =< aux(21)
s(60) =< s(45)* (1/3)+s(54)
s(61) =< s(45)* (1/5)+s(55)
s(62) =< s(45)* (1/5)+s(55)
s(60) =< s(45)* (1/5)+s(55)

with precondition: [V>=0]

* Chain [43]: 1
with precondition: [V=0,V3>=1]

* Chain [42]: 1*s(65)+1*s(66)+0
Such that:s(65) =< V3
s(66) =< V3+1

with precondition: [V=V3,V>=1]

* Chain [41]: 0
with precondition: [V=1,V3=2]

* Chain [40]: 0
with precondition: [V=2,V3=1]

* Chain [39]: 0
with precondition: [V=2,V3=2]

* Chain [38]: 1
with precondition: [V3=0,V>=1]


Closed-form bounds of start(V,V3):
-------------------------------------
* Chain [44] with precondition: [V>=0]
- Upper bound: 3*V+1+nat(V3)+ (3*V+3)+nat(V3+1)*9+nat(2/5*V+2/5*V3)*2+17/5*nat(V/3+V3/3+2/3)+ (V+1)+nat(V/3+V3/3)
- Complexity: n
* Chain [43] with precondition: [V=0,V3>=1]
- Upper bound: 1
- Complexity: constant
* Chain [42] with precondition: [V=V3,V>=1]
- Upper bound: 2*V3+1
- Complexity: n
* Chain [41] with precondition: [V=1,V3=2]
- Upper bound: 0
- Complexity: constant
* Chain [40] with precondition: [V=2,V3=1]
- Upper bound: 0
- Complexity: constant
* Chain [39] with precondition: [V=2,V3=2]
- Upper bound: 0
- Complexity: constant
* Chain [38] with precondition: [V3=0,V>=1]
- Upper bound: 1
- Complexity: constant

### Maximum cost of start(V,V3): max([1,6*V+4+nat(V3+1)*8+nat(2/5*V+2/5*V3)*2+17/5*nat(V/3+V3/3+2/3)+ (V+1)+nat(V/3+V3/3)+ (nat(V3+1)+nat(V3))])
Asymptotic class: n
* Total analysis performed in 591 ms.

(10) BOUNDS(1, n^1)